package ch.epfl.lara.matcheck.util.printer

import ch.epfl.lara.matcheck.ast.Formula
import ch.epfl.lara.matcheck.verify._

object PrettyStringerVTree extends FormatterTrees[VTree] { 
  
  
  override protected def format(vtree: VTree): String = vtree match {
    case VProgram(constr,containers) => 
      annotationformat("constraint")(constr) + NL + 
      "/** classes/objects declaration */" + NL + 
      concat(containers) 
      
    case VContainer(inv,methods) =>
      "Container {" + inc + NL + 
        annotationformat("invariant")(inv) + NL + 
        concat(methods) + dec + NL + 
      "}" + NL
      
    case VMethodDef(declaration,ppc,body) =>
      val annotation = ppc match {
        case None => ""  
        case Some((pre,post)) => NL +
          "/* precondition  " + PrettyStringerFormula.toString(pre) + NL +
          "   postcondition " + PrettyStringerFormula.toString(post) + NL + "*/"  
      }
      NL + "Method" + 
        annotation + NL +
      "{" + inc + NL +
        format(body) + dec + NL +
      "}" + NL 
      
    case VMatch(scrutinee, cases) =>
      "(" + PrettyStringerFormula.toString(scrutinee) + ") match { " + inc + NL +
        cases.map(format(_)).mkString(NL) + dec + NL +
      "}" + ")"
        
    
        
    case VIf((decl,cond),then,elze) => 
      "if (" + PrettyStringerFormula.toString(decl) + " --> " + PrettyStringerFormula.toString(cond) + ") {" + inc + NL +
        format(then) + dec + NL +
      "} else {" + inc + NL +
        format(elze) + dec + NL + 
      "}" + NL
    
    case VSimpleExpr => "se" 
  }
  
  
  protected def format (vcase: VCaseDef): String = {
    val VCaseDef(_,formula,body) = vcase
    PrettyStringerFormula.toString(formula) + " => " + inc + NL + 
    format(body) + dec + NL
  }
  
  private def annotationformat(prefix: String)(tree: Option[Formula]): String = tree match {
    case None => ""
    case Some(term) => "/*" + prefix + PrettyStringerFormula.toString(term) + "*/" + NL
  }
}
